(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 15))
(declare-fun v1 () (_ BitVec 29))
(declare-fun v2 () (_ BitVec 84))
(assert (let ((e3(_ bv3415463415813956548102973542979198 114)))
(let ((e4 (ite (bvsle e3 ((_ sign_extend 99) v0)) (_ bv1 1) (_ bv0 1))))
(let ((e5 (bvsub e3 ((_ sign_extend 30) v2))))
(let ((e6 (ite (distinct e5 e5) (_ bv1 1) (_ bv0 1))))
(let ((e7 (bvnot e5)))
(let ((e8 (bvxor ((_ zero_extend 113) e6) e5)))
(let ((e9 ((_ rotate_left 47) e3)))
(let ((e10 (bvurem ((_ zero_extend 113) e4) e7)))
(let ((e11 (bvmul e8 e5)))
(let ((e12 (bvadd e9 e11)))
(let ((e13 (bvmul e11 ((_ sign_extend 30) v2))))
(let ((e14 (bvxor e13 e5)))
(let ((e15 (bvsub ((_ sign_extend 99) v0) e3)))
(let ((e16 (bvudiv e3 e10)))
(let ((e17 (ite (distinct e10 ((_ zero_extend 85) v1)) (_ bv1 1) (_ bv0 1))))
(let ((e18 (bvugt ((_ zero_extend 85) v1) e5)))
(let ((e19 (bvsle e8 e12)))
(let ((e20 (bvsge e5 e16)))
(let ((e21 (distinct e12 ((_ zero_extend 30) v2))))
(let ((e22 (bvult ((_ sign_extend 85) v1) e7)))
(let ((e23 (bvslt e6 e17)))
(let ((e24 (distinct ((_ sign_extend 113) e4) e13)))
(let ((e25 (bvult ((_ zero_extend 113) e17) e12)))
(let ((e26 (= e9 e11)))
(let ((e27 (bvsle e14 e10)))
(let ((e28 (bvsle e11 e15)))
(let ((e29 (bvult e9 e3)))
(let ((e30 (bvuge e14 e9)))
(let ((e31 (bvult ((_ sign_extend 113) e6) e7)))
(let ((e32 (bvuge ((_ zero_extend 83) e6) v2)))
(let ((e33 (bvslt e10 e13)))
(let ((e34 (bvult ((_ zero_extend 85) v1) e13)))
(let ((e35 (bvugt e11 e3)))
(let ((e36 (bvsge e8 e14)))
(let ((e37 (bvsle e16 ((_ sign_extend 99) v0))))
(let ((e38 (ite e26 e26 e32)))
(let ((e39 (ite e31 e34 e23)))
(let ((e40 (=> e20 e33)))
(let ((e41 (or e35 e38)))
(let ((e42 (not e28)))
(let ((e43 (xor e18 e24)))
(let ((e44 (xor e37 e27)))
(let ((e45 (xor e29 e21)))
(let ((e46 (and e39 e40)))
(let ((e47 (=> e41 e22)))
(let ((e48 (xor e46 e47)))
(let ((e49 (= e43 e42)))
(let ((e50 (or e30 e49)))
(let ((e51 (=> e36 e36)))
(let ((e52 (= e19 e50)))
(let ((e53 (xor e25 e45)))
(let ((e54 (xor e51 e44)))
(let ((e55 (not e48)))
(let ((e56 (and e52 e55)))
(let ((e57 (=> e54 e56)))
(let ((e58 (and e57 e57)))
(let ((e59 (and e53 e53)))
(let ((e60 (not e59)))
(let ((e61 (= e60 e58)))
(let ((e62 (and e61 (not (= e10 (_ bv0 114))))))
(let ((e63 (and e62 (not (= e7 (_ bv0 114))))))
e63
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
